Bugfix/static function #739

NlightNFotis · 2017-03-30T17:24:54Z

Greetings,

This pull request contains a fix for the issue reported in pr #718. This contains the fix, changes for the tests so that they are now active, along with two more tests that show that goto-cc now correctly reports ambiguity that arises due to usage of the qualifier static between two functions with the same name and signature but in two different translation units.

Paging @martin-cs to add some concerns he has and @tautschnig for reviewing the solution.

tautschnig · 2017-03-30T18:32:51Z

src/goto-programs/goto_inline.cpp

+      // We also don't allow for the _start function to have any of its
+      // function calls to be inlined
+      if(!goto_function.body_available() ||
+         f_it->first==ID__start)


Do not use ID__start directly, use goto_functions.entry_point() instead.

tautschnig · 2017-03-30T18:35:47Z

src/linking/remove_internal_symbols.cpp

@@ -149,7 +150,7 @@ void remove_internal_symbols(
    else if(is_function)
    {
      // body? not local (i.e., "static")?
-      if(has_body && !is_file_local)
+      if(has_body || (!is_file_local && (config.main == symbol.name.c_str())))


That logic appears wrong to me - shouldn't this code be:

if(has_body && (!is_file_local || config.main==symbol.name))

I agree - & since this wasn't picked up by the tests I suggest adding an additional test that verifies an unused static function with body is correctly removed.

Yes, after discussing it with @thk123 it appears that I had understood the initial condition wrong, and thought that we should include a function "if it has a body or ...". Thomas let me know that this is wrong, and that if it has no body it's useless to us, so you're right. It will be updated accordingly.

thk123

I don't think the test would fail under the old logic.

thk123 · 2017-03-31T11:07:08Z

regression/ansi-c/static4/main.c

@@ -0,0 +1 @@
+static int foo(int a);


The symbol would still be included with the old logic since it is both static and without body. The function should have a body and should still be excluded.

tautschnig · 2017-03-31T12:12:30Z

@kroening Still left to decide whether this behaviour is actually desirable, i.e., whether functions marked "static" constitute valid entry points at all.

thk123 · 2017-03-31T13:16:11Z

@tautschnig Reason for needing this is for generating the test suite for a static function is useful when trying to generate unit tests.

peterschrammel · 2017-03-31T13:18:06Z

@thk123, how do you run these tests?

NlightNFotis · 2017-03-31T13:31:41Z

@peterschrammel We talked with thk123 about it, and the simple solution is to include the .c file in the test (as we already do) if the function is static.

kroening · 2017-04-01T19:15:20Z

src/linking/remove_internal_symbols.cpp

@@ -149,7 +150,8 @@ void remove_internal_symbols(
    else if(is_function)
    {
      // body? not local (i.e., "static")?
-      if(has_body && !is_file_local)
+      if(has_body &&
+         (!is_file_local || (config.main==symbol.name.c_str())))
        get_symbols_rec(ns, symbol, exported);


What's the .c_str() doing?

@kroening It's returning a const char * that we can compare to the std::string that is config.main. Without it, we get the following error message:

remove_internal_symbols.cpp: In function 'void remove_internal_symbols(symbol_tablet&)': remove_internal_symbols.cpp:153:54: error: no match for 'operator==' (operand types are 'std::__cxx11::string {aka std::__cxx11::basic_string<char>}' and 'const irep_idt {aka const dstringt}') if(has_body || (!is_file_local && (config.main == symbol.name)))

If we need to change it, I can change the c_str() call to as_string(), but they appear to do exactly the same thing, with the difference that c_str() returns a C string whereas as_string() returns a c++ string.

@kroening @NlightNFotis I'm wondering why config.main is a string. I can't see a good reason for it not to be an irep_idt.

martin-cs · 2017-04-03T14:02:15Z

<snip>

Paging @martin-cs to add some concerns he has and @tautschnig for reviewing the solution.

For the record... I wondered why we were removing functions at this early stage and when our general principle is to keep things as they are in the front-end and then only transform when we actually need to. It occurred to me that this was likely in the linker because it was implementing the semantics of linking (which symbols are included in shared libraries, etc.). The situation we want to support is clearly not something a C linker would (directly) do but I worried that we might break something if we changed the semantics. Given the review this has had I have no particular concerns with the current state of things, I just said I would comment on this.

kroening · 2017-04-04T12:45:41Z

Sorry, don't see why inlining into the _start function is a problem?

thk123 · 2017-04-04T13:17:52Z

@kroening Unfortunately the original PR for this change has been lost - but from memory and based off the commit message, the problem was to do with the interpreter not recording entering and exiting a function as it never entered the function. This commit is in test-gen-support so perhaps it shouldn't be back ported to CBMC?

When the partial inlining comes to the _Start function, it skips over it. We don't want inlining on the start function because if we are trying to find the entry point for the users code, it is important it hasn't been inlined into GOTO generated code.

…elected as the entry point and changed the tests to CORE rather than KNOWNBUG

…n error when a symbol ambiguity due to static arises.

…nternal_symbols static condition.

tautschnig requested changes Mar 30, 2017

View reviewed changes

NlightNFotis force-pushed the bugfix/static_function branch from 5b996c0 to 1a657b5 Compare March 31, 2017 10:38

thk123 suggested changes Mar 31, 2017

View reviewed changes

NlightNFotis force-pushed the bugfix/static_function branch from df86a4c to dbcff69 Compare March 31, 2017 11:25

tautschnig approved these changes Mar 31, 2017

View reviewed changes

tautschnig assigned kroening Mar 31, 2017

thk123 approved these changes Mar 31, 2017

View reviewed changes

kroening reviewed Apr 1, 2017

View reviewed changes

thk123 and others added 4 commits April 18, 2017 11:17

Fixed the issue with a single static function in a translation unit s…

96e2a84

…elected as the entry point and changed the tests to CORE rather than KNOWNBUG

Added two new tests that demonstrate that goto-cc correctly reports a…

6509e10

…n error when a symbol ambiguity due to static arises.

Added a new test that would fail with the wrong logic in the remove_i…

62995f5

…nternal_symbols static condition.

NlightNFotis force-pushed the bugfix/static_function branch from dbcff69 to 62995f5 Compare April 18, 2017 10:25

kroening merged commit 94e833d into diffblue:master Apr 19, 2017

Bugfix/static function #739

Bugfix/static function #739

Uh oh!

Conversation

NlightNFotis commented Mar 30, 2017

Uh oh!

tautschnig Mar 30, 2017

Choose a reason for hiding this comment

Uh oh!

tautschnig Mar 30, 2017

Choose a reason for hiding this comment

Uh oh!

thk123 Mar 31, 2017

Choose a reason for hiding this comment

Uh oh!

NlightNFotis Mar 31, 2017

Choose a reason for hiding this comment

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

thk123 Mar 31, 2017 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Mar 31, 2017

Uh oh!

thk123 commented Mar 31, 2017

Uh oh!

peterschrammel commented Mar 31, 2017

Uh oh!

NlightNFotis commented Mar 31, 2017 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

kroening Apr 1, 2017

Choose a reason for hiding this comment

Uh oh!

NlightNFotis Apr 3, 2017

Choose a reason for hiding this comment

Uh oh!

tautschnig Apr 3, 2017

Choose a reason for hiding this comment

Uh oh!

martin-cs commented Apr 3, 2017 via email

Uh oh!

kroening commented Apr 4, 2017

Uh oh!

thk123 commented Apr 4, 2017

Uh oh!

Uh oh!

thk123 Mar 31, 2017 •

edited

Loading

NlightNFotis commented Mar 31, 2017 •

edited

Loading